YES 2.769 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/List.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



↳ HASKELL
  ↳ LR

mainModule List
  ((elemIndex :: (Eq b, Eq a) => (b,a)  ->  [(b,a)]  ->  Maybe Int) :: (Eq b, Eq a) => (b,a)  ->  [(b,a)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (\vv1 ->
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []
) (zip xs (enumFrom 0))


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Lambda Reductions:
The following Lambda expression
\vv1→
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices0 p vv1 = 
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

The following Lambda expression
\ab→(a,b)

is transformed to
zip0 a b = (a,b)



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR

mainModule List
  ((elemIndex :: (Eq b, Eq a) => (a,b)  ->  [(a,b)]  ->  Maybe Int) :: (Eq a, Eq b) => (a,b)  ->  [(a,b)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = 
case vv1 of
  (x,i)->  if p x then i : [] else []
  _-> []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Case Reductions:
The following Case expression
case vv1 of
 (x,i) → if p x then i : [] else []
 _ → []

is transformed to
findIndices00 p (x,i) = if p x then i : [] else []
findIndices00 p _ = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR

mainModule List
  ((elemIndex :: (Eq a, Eq b) => (b,a)  ->  [(b,a)]  ->  Maybe Int) :: (Eq b, Eq a) => (b,a)  ->  [(b,a)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) =  if p x then i : [] else []
findIndices00 p _ = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



If Reductions:
The following If expression
if p x then i : [] else []

is transformed to
findIndices000 i True = i : []
findIndices000 i False = []



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR

mainModule List
  ((elemIndex :: (Eq a, Eq b) => (b,a)  ->  [(b,a)]  ->  Maybe Int) :: (Eq a, Eq b) => (b,a)  ->  [(b,a)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p _ = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : _) = Just a



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR

mainModule List
  ((elemIndex :: (Eq b, Eq a) => (a,b)  ->  [(a,b)]  ->  Maybe Int) :: (Eq b, Eq a) => (a,b)  ->  [(a,b)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed

mainModule List
  ((elemIndex :: (Eq a, Eq b) => (a,b)  ->  [(a,b)]  ->  Maybe Int) :: (Eq b, Eq a) => (a,b)  ->  [(a,b)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom 0))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Num Reduction: All numbers are transformed to thier corresponding representation with Pos, Neg, Succ and Zero.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow

mainModule List
  (elemIndex :: (Eq b, Eq a) => (a,b)  ->  [(a,b)]  ->  Maybe Int)

module List where
  import qualified Maybe
import qualified Prelude
  elemIndex :: Eq a => a  ->  [a]  ->  Maybe Int
elemIndex x = findIndex (== x)

  findIndex :: (a  ->  Bool)  ->  [a]  ->  Maybe Int
findIndex p = Maybe.listToMaybe . findIndices p

  findIndices :: (a  ->  Bool)  ->  [a]  ->  [Int]
findIndices p xs = concatMap (findIndices0 p) (zip xs (enumFrom (Pos Zero)))

  
findIndices0 p vv1 = findIndices00 p vv1

  
findIndices00 p (x,i) = findIndices000 i (p x)
findIndices00 p vw = []

  
findIndices000 i True = i : []
findIndices000 i False = []


module Maybe where
  import qualified List
import qualified Prelude
  listToMaybe :: [a]  ->  Maybe a
listToMaybe [] = Nothing
listToMaybe (a : vx) = Just a



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primPlusNat(Succ(yv5700), Succ(yv4010000)) → new_primPlusNat(yv5700, yv4010000)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primMulNat(Succ(yv31000), Succ(yv401000)) → new_primMulNat(yv31000, Succ(yv401000))

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_primEqNat(Succ(yv3100), Succ(yv40100)) → new_primEqNat(yv3100, yv40100)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof
                              ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_esEs0(Right(yv310), Right(yv4010), de, app(app(ty_@2, eb), ec)) → new_esEs2(yv310, yv4010, eb, ec)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, bag, app(app(app(ty_@3, bbf), bbg), bbh)) → new_esEs3(yv312, yv4012, bbf, bbg, bbh)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), gb, app(app(ty_@2, gg), gh)) → new_esEs2(yv311, yv4011, gg, gh)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), gb, app(ty_Maybe, gc)) → new_esEs(yv311, yv4011, gc)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), app(ty_Maybe, hd), he) → new_esEs(yv310, yv4010, hd)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), app(ty_Maybe, bdc), bag, bcb) → new_esEs(yv310, yv4010, bdc)
new_esEs(Just(yv310), Just(yv4010), app(app(app(ty_@3, bg), bh), ca)) → new_esEs3(yv310, yv4010, bg, bh, ca)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, bag, app(ty_[], bbc)) → new_esEs1(yv312, yv4012, bbc)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), eg) → new_esEs1(yv311, yv4011, eg)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), app(app(ty_@2, baa), bab), he) → new_esEs2(yv310, yv4010, baa, bab)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), app(ty_[], fc)) → new_esEs1(yv310, yv4010, fc)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), gb, app(app(app(ty_@3, ha), hb), hc)) → new_esEs3(yv311, yv4011, ha, hb, hc)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, app(ty_[], bce), bcb) → new_esEs1(yv311, yv4011, bce)
new_esEs0(Left(yv310), Left(yv4010), app(app(app(ty_@3, db), dc), dd), cc) → new_esEs3(yv310, yv4010, db, dc, dd)
new_esEs(Just(yv310), Just(yv4010), app(ty_Maybe, ba)) → new_esEs(yv310, yv4010, ba)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), gb, app(app(ty_Either, gd), ge)) → new_esEs0(yv311, yv4011, gd, ge)
new_esEs0(Left(yv310), Left(yv4010), app(app(ty_Either, cd), ce), cc) → new_esEs0(yv310, yv4010, cd, ce)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, app(ty_Maybe, bca), bcb) → new_esEs(yv311, yv4011, bca)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), app(ty_[], hh), he) → new_esEs1(yv310, yv4010, hh)
new_esEs0(Left(yv310), Left(yv4010), app(app(ty_@2, cg), da), cc) → new_esEs2(yv310, yv4010, cg, da)
new_esEs0(Right(yv310), Right(yv4010), de, app(app(app(ty_@3, ed), ee), ef)) → new_esEs3(yv310, yv4010, ed, ee, ef)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, bag, app(ty_Maybe, bah)) → new_esEs(yv312, yv4012, bah)
new_esEs0(Right(yv310), Right(yv4010), de, app(app(ty_Either, dg), dh)) → new_esEs0(yv310, yv4010, dg, dh)
new_esEs(Just(yv310), Just(yv4010), app(app(ty_Either, bb), bc)) → new_esEs0(yv310, yv4010, bb, bc)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, app(app(app(ty_@3, bch), bda), bdb), bcb) → new_esEs3(yv311, yv4011, bch, bda, bdb)
new_esEs(Just(yv310), Just(yv4010), app(app(ty_@2, be), bf)) → new_esEs2(yv310, yv4010, be, bf)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), app(app(ty_Either, fa), fb)) → new_esEs0(yv310, yv4010, fa, fb)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, bag, app(app(ty_@2, bbd), bbe)) → new_esEs2(yv312, yv4012, bbd, bbe)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, app(app(ty_@2, bcf), bcg), bcb) → new_esEs2(yv311, yv4011, bcf, bcg)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), app(app(ty_@2, bdg), bdh), bag, bcb) → new_esEs2(yv310, yv4010, bdg, bdh)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), app(ty_Maybe, eh)) → new_esEs(yv310, yv4010, eh)
new_esEs0(Right(yv310), Right(yv4010), de, app(ty_[], ea)) → new_esEs1(yv310, yv4010, ea)
new_esEs(Just(yv310), Just(yv4010), app(ty_[], bd)) → new_esEs1(yv310, yv4010, bd)
new_esEs0(Left(yv310), Left(yv4010), app(ty_[], cf), cc) → new_esEs1(yv310, yv4010, cf)
new_esEs0(Right(yv310), Right(yv4010), de, app(ty_Maybe, df)) → new_esEs(yv310, yv4010, df)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), app(app(app(ty_@3, fg), fh), ga)) → new_esEs3(yv310, yv4010, fg, fh, ga)
new_esEs1(:(yv310, yv311), :(yv4010, yv4011), app(app(ty_@2, fd), ff)) → new_esEs2(yv310, yv4010, fd, ff)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), app(ty_[], bdf), bag, bcb) → new_esEs1(yv310, yv4010, bdf)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), app(app(ty_Either, hf), hg), he) → new_esEs0(yv310, yv4010, hf, hg)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), gb, app(ty_[], gf)) → new_esEs1(yv311, yv4011, gf)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, app(app(ty_Either, bcc), bcd), bcb) → new_esEs0(yv311, yv4011, bcc, bcd)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), baf, bag, app(app(ty_Either, bba), bbb)) → new_esEs0(yv312, yv4012, bba, bbb)
new_esEs0(Left(yv310), Left(yv4010), app(ty_Maybe, cb), cc) → new_esEs(yv310, yv4010, cb)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), app(app(app(ty_@3, bea), beb), bec), bag, bcb) → new_esEs3(yv310, yv4010, bea, beb, bec)
new_esEs2(@2(yv310, yv311), @2(yv4010, yv4011), app(app(app(ty_@3, bac), bad), bae), he) → new_esEs3(yv310, yv4010, bac, bad, bae)
new_esEs3(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), app(app(ty_Either, bdd), bde), bag, bcb) → new_esEs0(yv310, yv4010, bdd, bde)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: 



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ CR
        ↳ HASKELL
          ↳ IFR
            ↳ HASKELL
              ↳ BR
                ↳ HASKELL
                  ↳ COR
                    ↳ HASKELL
                      ↳ NumRed
                        ↳ HASKELL
                          ↳ Narrow
                            ↳ AND
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                              ↳ QDP
                                ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_listToMaybe(yv41, False, yv22, yv23, :(yv24110, yv24111), ba, bb) → new_listToMaybe(new_primPlusNat0(yv41, Zero), new_esEs4(@2(yv22, yv23), yv24110, ba, bb), yv22, yv23, yv24111, ba, bb)

The TRS R consists of the following rules:

new_esEs25(yv310, yv4010, app(ty_[], bdh)) → new_esEs14(yv310, yv4010, bdh)
new_esEs23(yv310, yv4010, ty_Float) → new_esEs13(yv310, yv4010)
new_esEs18(Left(yv310), Left(yv4010), ty_Integer, cg) → new_esEs10(yv310, yv4010)
new_primPlusNat1(Succ(yv5700), Succ(yv4010000)) → Succ(Succ(new_primPlusNat1(yv5700, yv4010000)))
new_primEqInt(Neg(Succ(yv3100)), Pos(yv4010)) → False
new_primEqInt(Pos(Succ(yv3100)), Neg(yv4010)) → False
new_esEs21(yv312, yv4012, app(ty_Maybe, gb)) → new_esEs16(yv312, yv4012, gb)
new_esEs23(yv310, yv4010, ty_Ordering) → new_esEs11(yv310, yv4010)
new_esEs24(yv311, yv4011, app(app(ty_@2, bcg), bch)) → new_esEs4(yv311, yv4011, bcg, bch)
new_esEs25(yv310, yv4010, app(app(app(ty_@3, bec), bed), bee)) → new_esEs20(yv310, yv4010, bec, bed, bee)
new_esEs18(Left(yv310), Left(yv4010), app(ty_Maybe, da), cg) → new_esEs16(yv310, yv4010, da)
new_esEs18(Left(yv310), Left(yv4010), app(app(ty_Either, dc), dd), cg) → new_esEs18(yv310, yv4010, dc, dd)
new_esEs23(yv310, yv4010, app(app(ty_@2, bbc), bbd)) → new_esEs4(yv310, yv4010, bbc, bbd)
new_esEs25(yv310, yv4010, ty_Char) → new_esEs12(yv310, yv4010)
new_esEs24(yv311, yv4011, app(app(ty_Either, bcd), bce)) → new_esEs18(yv311, yv4011, bcd, bce)
new_esEs24(yv311, yv4011, ty_Ordering) → new_esEs11(yv311, yv4011)
new_primEqInt(Neg(Zero), Pos(Succ(yv40100))) → False
new_primEqInt(Pos(Zero), Neg(Succ(yv40100))) → False
new_esEs18(Right(yv310), Right(yv4010), ec, app(ty_[], eh)) → new_esEs14(yv310, yv4010, eh)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_@0) → new_esEs17(yv310, yv4010)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Integer) → new_esEs10(yv310, yv4010)
new_esEs21(yv312, yv4012, ty_Ordering) → new_esEs11(yv312, yv4012)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Char) → new_esEs12(yv310, yv4010)
new_esEs18(Right(yv310), Right(yv4010), ec, app(app(app(ty_@3, fc), fd), ff)) → new_esEs20(yv310, yv4010, fc, fd, ff)
new_esEs22(yv311, yv4011, ty_Char) → new_esEs12(yv311, yv4011)
new_esEs11(EQ, EQ) → True
new_esEs21(yv312, yv4012, ty_@0) → new_esEs17(yv312, yv4012)
new_primMulNat0(Zero, Zero) → Zero
new_esEs16(Nothing, Nothing, bef) → True
new_esEs22(yv311, yv4011, app(app(ty_Either, hf), hg)) → new_esEs18(yv311, yv4011, hf, hg)
new_esEs12(Char(yv310), Char(yv4010)) → new_primEqNat0(yv310, yv4010)
new_esEs25(yv310, yv4010, app(app(ty_@2, bea), beb)) → new_esEs4(yv310, yv4010, bea, beb)
new_primPlusNat0(Zero, yv401000) → Succ(yv401000)
new_esEs25(yv310, yv4010, app(ty_Ratio, bde)) → new_esEs6(yv310, yv4010, bde)
new_esEs11(LT, GT) → False
new_esEs11(GT, LT) → False
new_esEs15(yv310, yv4010, app(app(ty_Either, bg), bh)) → new_esEs18(yv310, yv4010, bg, bh)
new_esEs22(yv311, yv4011, ty_@0) → new_esEs17(yv311, yv4011)
new_esEs25(yv310, yv4010, ty_Ordering) → new_esEs11(yv310, yv4010)
new_esEs24(yv311, yv4011, app(ty_[], bcf)) → new_esEs14(yv311, yv4011, bcf)
new_esEs25(yv310, yv4010, ty_Integer) → new_esEs10(yv310, yv4010)
new_sr(Pos(yv3100), Neg(yv40100)) → Neg(new_primMulNat0(yv3100, yv40100))
new_sr(Neg(yv3100), Pos(yv40100)) → Neg(new_primMulNat0(yv3100, yv40100))
new_esEs16(Just(yv310), Just(yv4010), ty_Integer) → new_esEs10(yv310, yv4010)
new_esEs11(EQ, LT) → False
new_esEs11(LT, EQ) → False
new_esEs20(@3(yv310, yv311, yv312), @3(yv4010, yv4011, yv4012), fg, fh, ga) → new_asAs(new_esEs23(yv310, yv4010, fg), new_asAs(new_esEs22(yv311, yv4011, fh), new_esEs21(yv312, yv4012, ga)))
new_esEs16(Just(yv310), Just(yv4010), app(ty_Maybe, beg)) → new_esEs16(yv310, yv4010, beg)
new_esEs16(Just(yv310), Just(yv4010), app(app(app(ty_@3, bff), bfg), bfh)) → new_esEs20(yv310, yv4010, bff, bfg, bfh)
new_esEs15(yv310, yv4010, app(app(ty_@2, cb), cc)) → new_esEs4(yv310, yv4010, cb, cc)
new_esEs21(yv312, yv4012, app(ty_Ratio, gc)) → new_esEs6(yv312, yv4012, gc)
new_esEs22(yv311, yv4011, app(ty_Ratio, he)) → new_esEs6(yv311, yv4011, he)
new_esEs21(yv312, yv4012, ty_Bool) → new_esEs5(yv312, yv4012)
new_esEs4(@2(yv310, yv311), @2(yv4010, yv4011), bbh, bca) → new_asAs(new_esEs25(yv310, yv4010, bbh), new_esEs24(yv311, yv4011, bca))
new_esEs23(yv310, yv4010, ty_Integer) → new_esEs10(yv310, yv4010)
new_esEs21(yv312, yv4012, app(app(ty_@2, gg), gh)) → new_esEs4(yv312, yv4012, gg, gh)
new_esEs15(yv310, yv4010, ty_Bool) → new_esEs5(yv310, yv4010)
new_esEs18(Left(yv310), Left(yv4010), app(app(app(ty_@3, dh), ea), eb), cg) → new_esEs20(yv310, yv4010, dh, ea, eb)
new_esEs24(yv311, yv4011, ty_@0) → new_esEs17(yv311, yv4011)
new_esEs15(yv310, yv4010, ty_Float) → new_esEs13(yv310, yv4010)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Ordering) → new_esEs11(yv310, yv4010)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Bool) → new_esEs5(yv310, yv4010)
new_esEs16(Just(yv310), Just(yv4010), ty_Bool) → new_esEs5(yv310, yv4010)
new_esEs18(Left(yv310), Left(yv4010), ty_Char, cg) → new_esEs12(yv310, yv4010)
new_esEs22(yv311, yv4011, ty_Integer) → new_esEs10(yv311, yv4011)
new_esEs22(yv311, yv4011, app(ty_[], hh)) → new_esEs14(yv311, yv4011, hh)
new_esEs15(yv310, yv4010, ty_Ordering) → new_esEs11(yv310, yv4010)
new_esEs18(Left(yv310), Left(yv4010), ty_Int, cg) → new_esEs9(yv310, yv4010)
new_esEs19(Double(yv310, yv311), Double(yv4010, yv4011)) → new_esEs9(new_sr(yv310, yv4010), new_sr(yv311, yv4011))
new_esEs18(Left(yv310), Left(yv4010), app(ty_Ratio, db), cg) → new_esEs6(yv310, yv4010, db)
new_primEqNat0(Succ(yv3100), Zero) → False
new_primEqNat0(Zero, Succ(yv40100)) → False
new_esEs21(yv312, yv4012, ty_Int) → new_esEs9(yv312, yv4012)
new_esEs16(Just(yv310), Just(yv4010), app(app(ty_Either, bfa), bfb)) → new_esEs18(yv310, yv4010, bfa, bfb)
new_esEs17(@0, @0) → True
new_esEs25(yv310, yv4010, ty_Float) → new_esEs13(yv310, yv4010)
new_primEqInt(Pos(Zero), Pos(Zero)) → True
new_esEs21(yv312, yv4012, ty_Integer) → new_esEs10(yv312, yv4012)
new_esEs10(Integer(yv310), Integer(yv4010)) → new_primEqInt(yv310, yv4010)
new_esEs14([], [], bd) → True
new_esEs18(Left(yv310), Left(yv4010), ty_Ordering, cg) → new_esEs11(yv310, yv4010)
new_esEs22(yv311, yv4011, ty_Int) → new_esEs9(yv311, yv4011)
new_esEs7(yv311, yv4011, ty_Integer) → new_esEs10(yv311, yv4011)
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Float) → new_esEs13(yv310, yv4010)
new_esEs24(yv311, yv4011, ty_Double) → new_esEs19(yv311, yv4011)
new_esEs23(yv310, yv4010, app(ty_[], bbb)) → new_esEs14(yv310, yv4010, bbb)
new_esEs22(yv311, yv4011, app(app(ty_@2, baa), bab)) → new_esEs4(yv311, yv4011, baa, bab)
new_esEs23(yv310, yv4010, app(ty_Ratio, bag)) → new_esEs6(yv310, yv4010, bag)
new_esEs24(yv311, yv4011, ty_Int) → new_esEs9(yv311, yv4011)
new_esEs8(yv310, yv4010, ty_Integer) → new_esEs10(yv310, yv4010)
new_esEs24(yv311, yv4011, app(ty_Ratio, bcc)) → new_esEs6(yv311, yv4011, bcc)
new_esEs21(yv312, yv4012, app(app(ty_Either, gd), ge)) → new_esEs18(yv312, yv4012, gd, ge)
new_esEs18(Left(yv310), Left(yv4010), app(app(ty_@2, df), dg), cg) → new_esEs4(yv310, yv4010, df, dg)
new_esEs23(yv310, yv4010, ty_Bool) → new_esEs5(yv310, yv4010)
new_esEs15(yv310, yv4010, ty_Integer) → new_esEs10(yv310, yv4010)
new_esEs21(yv312, yv4012, ty_Double) → new_esEs19(yv312, yv4012)
new_esEs18(Right(yv310), Right(yv4010), ec, app(ty_Ratio, ee)) → new_esEs6(yv310, yv4010, ee)
new_esEs21(yv312, yv4012, ty_Float) → new_esEs13(yv312, yv4012)
new_esEs18(Right(yv310), Right(yv4010), ec, app(app(ty_@2, fa), fb)) → new_esEs4(yv310, yv4010, fa, fb)
new_esEs11(GT, GT) → True
new_esEs23(yv310, yv4010, ty_Double) → new_esEs19(yv310, yv4010)
new_sr(Neg(yv3100), Neg(yv40100)) → Pos(new_primMulNat0(yv3100, yv40100))
new_esEs14(:(yv310, yv311), :(yv4010, yv4011), bd) → new_asAs(new_esEs15(yv310, yv4010, bd), new_esEs14(yv311, yv4011, bd))
new_sr(Pos(yv3100), Pos(yv40100)) → Pos(new_primMulNat0(yv3100, yv40100))
new_asAs(False, yv56) → False
new_primEqNat0(Zero, Zero) → True
new_esEs16(Just(yv310), Just(yv4010), app(ty_Ratio, beh)) → new_esEs6(yv310, yv4010, beh)
new_primMulNat0(Succ(yv31000), Zero) → Zero
new_primMulNat0(Zero, Succ(yv401000)) → Zero
new_esEs8(yv310, yv4010, ty_Int) → new_esEs9(yv310, yv4010)
new_esEs18(Left(yv310), Left(yv4010), ty_Double, cg) → new_esEs19(yv310, yv4010)
new_esEs16(Just(yv310), Just(yv4010), ty_@0) → new_esEs17(yv310, yv4010)
new_esEs18(Right(yv310), Right(yv4010), ec, app(app(ty_Either, ef), eg)) → new_esEs18(yv310, yv4010, ef, eg)
new_esEs16(Just(yv310), Just(yv4010), ty_Char) → new_esEs12(yv310, yv4010)
new_esEs23(yv310, yv4010, ty_Int) → new_esEs9(yv310, yv4010)
new_esEs15(yv310, yv4010, ty_Int) → new_esEs9(yv310, yv4010)
new_esEs25(yv310, yv4010, ty_Bool) → new_esEs5(yv310, yv4010)
new_esEs25(yv310, yv4010, app(app(ty_Either, bdf), bdg)) → new_esEs18(yv310, yv4010, bdf, bdg)
new_esEs5(False, False) → True
new_esEs5(True, False) → False
new_esEs5(False, True) → False
new_esEs24(yv311, yv4011, app(ty_Maybe, bcb)) → new_esEs16(yv311, yv4011, bcb)
new_esEs16(Just(yv310), Just(yv4010), ty_Float) → new_esEs13(yv310, yv4010)
new_esEs23(yv310, yv4010, app(app(app(ty_@3, bbe), bbf), bbg)) → new_esEs20(yv310, yv4010, bbe, bbf, bbg)
new_esEs18(Left(yv310), Right(yv4010), ec, cg) → False
new_esEs18(Right(yv310), Left(yv4010), ec, cg) → False
new_esEs16(Just(yv310), Just(yv4010), app(app(ty_@2, bfd), bfe)) → new_esEs4(yv310, yv4010, bfd, bfe)
new_esEs23(yv310, yv4010, ty_Char) → new_esEs12(yv310, yv4010)
new_esEs16(Just(yv310), Just(yv4010), app(ty_[], bfc)) → new_esEs14(yv310, yv4010, bfc)
new_esEs24(yv311, yv4011, ty_Char) → new_esEs12(yv311, yv4011)
new_primPlusNat0(Succ(yv570), yv401000) → Succ(Succ(new_primPlusNat1(yv570, yv401000)))
new_esEs24(yv311, yv4011, ty_Integer) → new_esEs10(yv311, yv4011)
new_esEs5(True, True) → True
new_esEs21(yv312, yv4012, app(app(app(ty_@3, ha), hb), hc)) → new_esEs20(yv312, yv4012, ha, hb, hc)
new_primEqInt(Neg(Succ(yv3100)), Neg(Succ(yv40100))) → new_primEqNat0(yv3100, yv40100)
new_esEs15(yv310, yv4010, ty_@0) → new_esEs17(yv310, yv4010)
new_esEs24(yv311, yv4011, app(app(app(ty_@3, bda), bdb), bdc)) → new_esEs20(yv311, yv4011, bda, bdb, bdc)
new_esEs18(Right(yv310), Right(yv4010), ec, app(ty_Maybe, ed)) → new_esEs16(yv310, yv4010, ed)
new_esEs22(yv311, yv4011, ty_Bool) → new_esEs5(yv311, yv4011)
new_primPlusNat1(Zero, Succ(yv4010000)) → Succ(yv4010000)
new_primPlusNat1(Succ(yv5700), Zero) → Succ(yv5700)
new_esEs23(yv310, yv4010, app(ty_Maybe, baf)) → new_esEs16(yv310, yv4010, baf)
new_esEs21(yv312, yv4012, ty_Char) → new_esEs12(yv312, yv4012)
new_esEs16(Just(yv310), Just(yv4010), ty_Ordering) → new_esEs11(yv310, yv4010)
new_esEs15(yv310, yv4010, app(ty_[], ca)) → new_esEs14(yv310, yv4010, ca)
new_esEs14([], :(yv4010, yv4011), bd) → False
new_esEs14(:(yv310, yv311), [], bd) → False
new_esEs15(yv310, yv4010, ty_Char) → new_esEs12(yv310, yv4010)
new_primEqInt(Neg(Zero), Neg(Zero)) → True
new_esEs7(yv311, yv4011, ty_Int) → new_esEs9(yv311, yv4011)
new_esEs18(Left(yv310), Left(yv4010), app(ty_[], de), cg) → new_esEs14(yv310, yv4010, de)
new_esEs16(Just(yv310), Nothing, bef) → False
new_esEs16(Nothing, Just(yv4010), bef) → False
new_esEs23(yv310, yv4010, app(app(ty_Either, bah), bba)) → new_esEs18(yv310, yv4010, bah, bba)
new_primEqInt(Neg(Zero), Neg(Succ(yv40100))) → False
new_primEqInt(Neg(Succ(yv3100)), Neg(Zero)) → False
new_esEs18(Left(yv310), Left(yv4010), ty_Bool, cg) → new_esEs5(yv310, yv4010)
new_esEs25(yv310, yv4010, ty_Double) → new_esEs19(yv310, yv4010)
new_esEs22(yv311, yv4011, ty_Float) → new_esEs13(yv311, yv4011)
new_esEs25(yv310, yv4010, app(ty_Maybe, bdd)) → new_esEs16(yv310, yv4010, bdd)
new_primPlusNat1(Zero, Zero) → Zero
new_asAs(True, yv56) → yv56
new_esEs16(Just(yv310), Just(yv4010), ty_Double) → new_esEs19(yv310, yv4010)
new_esEs22(yv311, yv4011, app(ty_Maybe, hd)) → new_esEs16(yv311, yv4011, hd)
new_primMulNat0(Succ(yv31000), Succ(yv401000)) → new_primPlusNat0(new_primMulNat0(yv31000, Succ(yv401000)), yv401000)
new_esEs13(Float(yv310, yv311), Float(yv4010, yv4011)) → new_esEs9(new_sr(yv310, yv4010), new_sr(yv311, yv4011))
new_esEs6(:%(yv310, yv311), :%(yv4010, yv4011), bc) → new_asAs(new_esEs8(yv310, yv4010, bc), new_esEs7(yv311, yv4011, bc))
new_esEs25(yv310, yv4010, ty_@0) → new_esEs17(yv310, yv4010)
new_esEs11(LT, LT) → True
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Int) → new_esEs9(yv310, yv4010)
new_primEqInt(Pos(Succ(yv3100)), Pos(Succ(yv40100))) → new_primEqNat0(yv3100, yv40100)
new_esEs18(Left(yv310), Left(yv4010), ty_Float, cg) → new_esEs13(yv310, yv4010)
new_esEs22(yv311, yv4011, app(app(app(ty_@3, bac), bad), bae)) → new_esEs20(yv311, yv4011, bac, bad, bae)
new_esEs24(yv311, yv4011, ty_Float) → new_esEs13(yv311, yv4011)
new_esEs15(yv310, yv4010, app(app(app(ty_@3, cd), ce), cf)) → new_esEs20(yv310, yv4010, cd, ce, cf)
new_esEs25(yv310, yv4010, ty_Int) → new_esEs9(yv310, yv4010)
new_esEs22(yv311, yv4011, ty_Double) → new_esEs19(yv311, yv4011)
new_esEs24(yv311, yv4011, ty_Bool) → new_esEs5(yv311, yv4011)
new_primEqNat0(Succ(yv3100), Succ(yv40100)) → new_primEqNat0(yv3100, yv40100)
new_esEs9(yv31, yv401) → new_primEqInt(yv31, yv401)
new_esEs11(EQ, GT) → False
new_esEs11(GT, EQ) → False
new_esEs21(yv312, yv4012, app(ty_[], gf)) → new_esEs14(yv312, yv4012, gf)
new_esEs15(yv310, yv4010, ty_Double) → new_esEs19(yv310, yv4010)
new_esEs15(yv310, yv4010, app(ty_Ratio, bf)) → new_esEs6(yv310, yv4010, bf)
new_esEs15(yv310, yv4010, app(ty_Maybe, be)) → new_esEs16(yv310, yv4010, be)
new_esEs18(Left(yv310), Left(yv4010), ty_@0, cg) → new_esEs17(yv310, yv4010)
new_primEqInt(Pos(Zero), Pos(Succ(yv40100))) → False
new_primEqInt(Pos(Succ(yv3100)), Pos(Zero)) → False
new_esEs22(yv311, yv4011, ty_Ordering) → new_esEs11(yv311, yv4011)
new_primEqInt(Neg(Zero), Pos(Zero)) → True
new_primEqInt(Pos(Zero), Neg(Zero)) → True
new_esEs18(Right(yv310), Right(yv4010), ec, ty_Double) → new_esEs19(yv310, yv4010)
new_esEs16(Just(yv310), Just(yv4010), ty_Int) → new_esEs9(yv310, yv4010)
new_esEs23(yv310, yv4010, ty_@0) → new_esEs17(yv310, yv4010)

The set Q consists of the following terms:

new_esEs24(x0, x1, ty_Int)
new_esEs18(Right(x0), Right(x1), x2, ty_Char)
new_esEs23(x0, x1, ty_Ordering)
new_primPlusNat0(Zero, x0)
new_esEs21(x0, x1, ty_Integer)
new_esEs25(x0, x1, app(ty_Ratio, x2))
new_esEs18(Left(x0), Left(x1), ty_Int, x2)
new_esEs25(x0, x1, app(app(ty_Either, x2), x3))
new_sr(Neg(x0), Neg(x1))
new_primEqInt(Pos(Zero), Neg(Zero))
new_primEqInt(Neg(Zero), Pos(Zero))
new_esEs16(Just(x0), Just(x1), app(ty_[], x2))
new_esEs15(x0, x1, ty_@0)
new_esEs18(Left(x0), Left(x1), app(ty_Ratio, x2), x3)
new_primPlusNat1(Succ(x0), Succ(x1))
new_esEs6(:%(x0, x1), :%(x2, x3), x4)
new_esEs25(x0, x1, ty_Float)
new_esEs24(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Bool)
new_esEs18(Right(x0), Right(x1), x2, ty_@0)
new_esEs25(x0, x1, ty_Integer)
new_esEs11(LT, EQ)
new_esEs11(EQ, LT)
new_sr(Neg(x0), Pos(x1))
new_sr(Pos(x0), Neg(x1))
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_Either, x3), x4))
new_esEs18(Right(x0), Right(x1), x2, ty_Int)
new_esEs24(x0, x1, ty_Float)
new_primEqInt(Neg(Zero), Neg(Zero))
new_esEs24(x0, x1, app(ty_Ratio, x2))
new_esEs7(x0, x1, ty_Int)
new_esEs25(x0, x1, ty_Char)
new_esEs18(Right(x0), Right(x1), x2, ty_Float)
new_esEs18(Left(x0), Left(x1), ty_Char, x2)
new_esEs16(Just(x0), Just(x1), ty_Double)
new_esEs25(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Left(x0), Left(x1), app(ty_[], x2), x3)
new_primMulNat0(Zero, Succ(x0))
new_esEs14([], :(x0, x1), x2)
new_esEs21(x0, x1, app(app(ty_Either, x2), x3))
new_esEs15(x0, x1, app(ty_[], x2))
new_esEs16(Nothing, Nothing, x0)
new_esEs25(x0, x1, app(ty_[], x2))
new_esEs24(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Int)
new_esEs23(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(Left(x0), Left(x1), ty_Bool, x2)
new_esEs21(x0, x1, app(ty_Ratio, x2))
new_primEqInt(Pos(Succ(x0)), Neg(x1))
new_primEqInt(Neg(Succ(x0)), Pos(x1))
new_esEs24(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs5(False, True)
new_esEs5(True, False)
new_esEs15(x0, x1, ty_Char)
new_esEs18(Right(x0), Left(x1), x2, x3)
new_esEs18(Left(x0), Right(x1), x2, x3)
new_esEs4(@2(x0, x1), @2(x2, x3), x4, x5)
new_esEs25(x0, x1, ty_Ordering)
new_esEs22(x0, x1, app(ty_Ratio, x2))
new_primPlusNat1(Succ(x0), Zero)
new_esEs21(x0, x1, app(ty_Maybe, x2))
new_esEs23(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs12(Char(x0), Char(x1))
new_esEs10(Integer(x0), Integer(x1))
new_esEs7(x0, x1, ty_Integer)
new_esEs15(x0, x1, ty_Int)
new_esEs22(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs16(Just(x0), Just(x1), ty_Ordering)
new_esEs15(x0, x1, ty_Integer)
new_primEqInt(Neg(Succ(x0)), Neg(Succ(x1)))
new_esEs24(x0, x1, ty_Ordering)
new_esEs21(x0, x1, ty_Double)
new_esEs21(x0, x1, ty_@0)
new_esEs25(x0, x1, app(ty_Maybe, x2))
new_esEs22(x0, x1, ty_Ordering)
new_esEs16(Just(x0), Just(x1), ty_Integer)
new_esEs22(x0, x1, ty_Integer)
new_esEs11(GT, EQ)
new_esEs11(EQ, GT)
new_esEs22(x0, x1, ty_Int)
new_esEs23(x0, x1, ty_Double)
new_esEs20(@3(x0, x1, x2), @3(x3, x4, x5), x6, x7, x8)
new_esEs23(x0, x1, ty_Float)
new_esEs15(x0, x1, ty_Double)
new_esEs23(x0, x1, app(ty_Ratio, x2))
new_esEs5(True, True)
new_esEs18(Right(x0), Right(x1), x2, app(ty_[], x3))
new_primEqNat0(Zero, Zero)
new_esEs18(Left(x0), Left(x1), ty_@0, x2)
new_esEs16(Just(x0), Just(x1), app(app(ty_Either, x2), x3))
new_esEs16(Just(x0), Just(x1), app(ty_Ratio, x2))
new_primEqNat0(Succ(x0), Zero)
new_primEqInt(Neg(Zero), Pos(Succ(x0)))
new_primEqInt(Pos(Zero), Neg(Succ(x0)))
new_esEs21(x0, x1, ty_Char)
new_esEs5(False, False)
new_esEs24(x0, x1, ty_Double)
new_esEs24(x0, x1, app(app(ty_Either, x2), x3))
new_esEs21(x0, x1, ty_Float)
new_esEs15(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Neg(Succ(x0)), Neg(Zero))
new_esEs18(Right(x0), Right(x1), x2, app(app(ty_@2, x3), x4))
new_esEs15(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Right(x0), Right(x1), x2, app(app(app(ty_@3, x3), x4), x5))
new_esEs15(x0, x1, ty_Float)
new_primMulNat0(Zero, Zero)
new_esEs22(x0, x1, app(app(ty_@2, x2), x3))
new_primEqInt(Pos(Succ(x0)), Pos(Succ(x1)))
new_esEs21(x0, x1, app(app(ty_@2, x2), x3))
new_esEs15(x0, x1, app(ty_Maybe, x2))
new_esEs25(x0, x1, ty_Double)
new_primEqInt(Pos(Succ(x0)), Pos(Zero))
new_esEs23(x0, x1, app(ty_Maybe, x2))
new_esEs16(Just(x0), Just(x1), ty_@0)
new_sr(Pos(x0), Pos(x1))
new_esEs25(x0, x1, ty_Int)
new_esEs18(Right(x0), Right(x1), x2, ty_Ordering)
new_esEs22(x0, x1, ty_@0)
new_esEs19(Double(x0, x1), Double(x2, x3))
new_esEs11(GT, GT)
new_esEs15(x0, x1, app(ty_Ratio, x2))
new_esEs8(x0, x1, ty_Int)
new_esEs16(Nothing, Just(x0), x1)
new_esEs15(x0, x1, app(app(ty_Either, x2), x3))
new_primMulNat0(Succ(x0), Zero)
new_esEs18(Left(x0), Left(x1), app(app(app(ty_@3, x2), x3), x4), x5)
new_esEs18(Left(x0), Left(x1), ty_Integer, x2)
new_esEs24(x0, x1, ty_Bool)
new_esEs14(:(x0, x1), :(x2, x3), x4)
new_primMulNat0(Succ(x0), Succ(x1))
new_primEqInt(Pos(Zero), Pos(Succ(x0)))
new_esEs11(GT, LT)
new_esEs11(LT, GT)
new_esEs8(x0, x1, ty_Integer)
new_esEs23(x0, x1, ty_@0)
new_asAs(False, x0)
new_esEs22(x0, x1, app(ty_[], x2))
new_esEs25(x0, x1, app(app(ty_@2, x2), x3))
new_primEqNat0(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Int)
new_esEs24(x0, x1, ty_@0)
new_esEs18(Right(x0), Right(x1), x2, ty_Double)
new_esEs18(Left(x0), Left(x1), app(ty_Maybe, x2), x3)
new_esEs22(x0, x1, ty_Double)
new_esEs18(Left(x0), Left(x1), ty_Ordering, x2)
new_esEs16(Just(x0), Just(x1), ty_Float)
new_esEs18(Right(x0), Right(x1), x2, app(ty_Ratio, x3))
new_esEs18(Right(x0), Right(x1), x2, ty_Integer)
new_primEqNat0(Succ(x0), Succ(x1))
new_esEs9(x0, x1)
new_esEs24(x0, x1, app(ty_[], x2))
new_esEs14(:(x0, x1), [], x2)
new_esEs16(Just(x0), Just(x1), app(ty_Maybe, x2))
new_primPlusNat1(Zero, Succ(x0))
new_esEs23(x0, x1, ty_Integer)
new_esEs21(x0, x1, ty_Ordering)
new_esEs23(x0, x1, ty_Bool)
new_esEs23(x0, x1, app(app(ty_Either, x2), x3))
new_esEs16(Just(x0), Just(x1), ty_Int)
new_esEs18(Left(x0), Left(x1), app(app(ty_@2, x2), x3), x4)
new_primPlusNat0(Succ(x0), x1)
new_esEs21(x0, x1, app(ty_[], x2))
new_esEs13(Float(x0, x1), Float(x2, x3))
new_esEs11(LT, LT)
new_esEs18(Right(x0), Right(x1), x2, ty_Bool)
new_esEs16(Just(x0), Just(x1), ty_Char)
new_esEs18(Left(x0), Left(x1), ty_Float, x2)
new_primPlusNat1(Zero, Zero)
new_esEs16(Just(x0), Just(x1), ty_Bool)
new_esEs22(x0, x1, app(app(ty_Either, x2), x3))
new_esEs25(x0, x1, ty_@0)
new_primEqInt(Pos(Zero), Pos(Zero))
new_esEs11(EQ, EQ)
new_esEs22(x0, x1, ty_Float)
new_esEs23(x0, x1, ty_Char)
new_esEs24(x0, x1, ty_Char)
new_asAs(True, x0)
new_esEs22(x0, x1, app(ty_Maybe, x2))
new_esEs15(x0, x1, ty_Ordering)
new_esEs16(Just(x0), Just(x1), app(app(ty_@2, x2), x3))
new_esEs23(x0, x1, app(ty_[], x2))
new_esEs16(Just(x0), Just(x1), app(app(app(ty_@3, x2), x3), x4))
new_esEs25(x0, x1, ty_Bool)
new_primEqInt(Neg(Zero), Neg(Succ(x0)))
new_esEs21(x0, x1, ty_Bool)
new_esEs17(@0, @0)
new_esEs24(x0, x1, app(app(ty_@2, x2), x3))
new_esEs18(Left(x0), Left(x1), app(app(ty_Either, x2), x3), x4)
new_esEs18(Right(x0), Right(x1), x2, app(ty_Maybe, x3))
new_esEs16(Just(x0), Nothing, x1)
new_esEs15(x0, x1, ty_Bool)
new_esEs21(x0, x1, app(app(app(ty_@3, x2), x3), x4))
new_esEs18(Left(x0), Left(x1), ty_Double, x2)
new_esEs14([], [], x0)
new_esEs22(x0, x1, ty_Char)

We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: